Processing math: 100%
We use cookies to improve your experience with our site.

Indexed in:

SCIE, EI, Scopus, INSPEC, DBLP, CSCD, etc.

Submission System
(Author / Reviewer / Editor)
Advanced Search
Volume 24 Issue 1
January  2009
Turn off MathJax
Article Contents
Abstract
References
Related Articles
Xian Xu. Expressing First-Order pi-Calculus in Higher-Order Calculus of Communicating Systems[J]. Journal of Computer Science and Technology, 2009, 24(1): 122-137.
Citation: Xian Xu. Expressing First-Order pi-Calculus in Higher-Order Calculus of Communicating Systems[J]. Journal of Computer Science and Technology, 2009, 24(1): 122-137.
shu

Expressing First-Order pi-Calculus in Higher-Order Calculus of Communicating Systems

  • Department of Computer Science and Engineering, Shanghai Jiao Tong University, Shanghai 200240, ChinaDepartment of Computer Science and Engineering, East China University of Science and Technology, Shanghai 200237, China

More Information
  • Received Date: July 06, 2007
  • Revised Date: July 08, 2008
  • Published Date: January 09, 2009
    Abstract
  • In the study of process calculi, encoding between different calculiis an effective way to compare the expressive power of calculi and canshed light on the essence of where the difference lies. Thomsen andSangiorgi have worked on the higher-order calculi (higher-order Calculusof Communicating Systems (CCS) and higher-order π-calculus, respectively) and the encodingfrom and to first-order π-calculus. However a fully abstractencoding of first-order π-calculus with higher-order CCS isnot available up-today. This is what we intend to settle in thispaper. We follow the encoding strategy, first proposed by Thomsen, oftranslating first-order π-calculus into Plain CHOCS. We show that theencoding strategy is fully abstract with respect to earlybisimilarity (first-order π-calculus) and wired bisimilarity(Plain CHOCS) (which is a bisimulation defined on wired processes only sendingand receiving wires), that is the core of the encoding strategy.Moreover from the fact that the wired bisimilarity is contained by thewell-established context bisimilarity, we secure the soundness ofthe encoding, with respect to early bisimilarity and contextbisimilarity. We use index technique to get around all the technicaldetails to reach these main results of this paper. Finally, we makesome discussion on our work and suggest some future work.
    • FullText(HTML)
    • References (18)
  • [1] Thomsen B. Plain CHOCS, a second generation calculus for higher-order processes. {\it Acta Informatica}, 1993, 30(1): 1--59.
    [2] Cao Z. More on bisimulations for higher order π-calculus. In {\it Proc. FOSSACS2006}, Vienna, Austria, Aceto L, In{\'g}olfsd{\'o}ttir A (eds.), {\it LNCS} 3921, 2006, pp.63--78.
    [3] Thomsen B. A calculus of higher order communication systems. In {\it Proc. POPL'89}, Austin, TX, USA, 1989, pp.143--154.
    [4] Thomsen B. Calculi for higher order communicating systems [Ph.D. Dissertation]. Department of Computing, Imperial College, 1990. %Administrator
    [5] Thomsen B. A theory of higher order communication systems. {\it Information and Computation}, 1995, 116: 38--57. %Administrator
    [6] Sangiorgi D. Expressing mobility in process algebras: First-order and higher-order paradigms [Ph.D. Dissertation]. University of Edinburgh, 1992. %Administrator
    [7] Sangiorgi D. From π-calculus to higher-order π-calculus---and back. In {\it Proc. TAPSOFT'93}, Orsay, France, {\it LNCS} 668, Springer Verlag, 1992, pp.151--166. %Administrator
    [8] Sangiorgi D. Bisimulation for higher-order process calculi. {\it Information and Computation}, 1996, 131(2): 141--178, Preliminary version: In {\it Proc. the IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET'94)}, \rm North Holland, 1994, pp.207--224. % owner = {Administrator},
    [9] Sangiorgi D, Walker D. On barbed equivalences in pi-calculus. In {\it Proc. CONCUR'01}, Aalborg, Denmark, {\it LNCS} 2154, 2001, pp.292--304. % owner = {Administrator},
    [10] Sangiorgi D, Walker D. The Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press, 2001. %Administrator,
    [11] Yongjian Li, Xinxin Liu. Towards a theory of bisimulation for the higher-order process calculi. {\it Journal of Computer Science and Technology}, May 2004, 19(3): 352--363. %Administrator
    [12] Yuxi Fu. Checking equivalence for higher order processes. Technical Report, SJTU BASICS, 2005. %Administrator
    [13] Milner R, Parrow J, Walker D. A calculus of mobile processes (Parts I and II). {\it Information and Computation}, 1992, 100(1): 1--77. %Administrator
    [14] Milner R. Functions as processes. {\it Journal of Mathematical Structures in Computer Science}, 1992, 2(2): 119--141. Research Report 1154, INRIA, Sofia Antipolis, 1990. %Administrator
    [15] Milner R. Communication and Concurrency. Prentice Hall, 1989. %Administrator
    [16] Sangiorgi D, Milner R. The problem of weak bisimulation up-to. In {\it Proc. CONCUR'92}, {\it LNCS} 630, 1992, pp.32--46. %Administrator
    [17] Milner R, Sangiorgi D. Barbed bisimulation. In {\it Proc. the 19th International Colloquium on Automata, Languages and Programming (ICALP'92)}, Vienna, Austria, {\it LNCS} 623, Springer Verlag, 1992, pp.685--695. %Administrator
    [18] Yuxi Fu. On quasi open bisimulation. {\it Theoretical Computer Science}, 2005, 338(1-3): 96--126.
    • Relative Articles

  • Related Articles

    [1]Zhong-Yi Wang, Ming-Shuai Chen, Teng-Jie Lin, Lin-Yu Yang, Jun-Hao Zhuo, Qiu-Ye Wang, Sheng-Chao Qin, Xiao Yi, Jian-Wei Yin. Parf: An Adaptive Abstraction-Strategy Tuner for Static Analysis[J]. Journal of Computer Science and Technology. DOI: 10.1007/s11390-025-5140-6
    [2]Heng-Feng Wei, Rui-Ze Tang, Yu Huang, Jian Lv. Jupiter Made Abstract, and Then Refined[J]. Journal of Computer Science and Technology, 2020, 35(6): 1343-1364. DOI: 10.1007/s11390-020-0516-0
    [3]Zu-Jie Ren, Ke Chen, Li-Dan Shou, Gang Chen, Yi-Jun Bei, Xiao-Yan Li. HAPS: Supporting Effective and Efficient Full-Text P2P Search with Peer Dynamics[J]. Journal of Computer Science and Technology, 2010, 25(3): 482-498.
    [4]Sa'ed Abed, Otmane Ait Mohamed, Ghiath Al-Sammane. An Abstract Reachability Approach by Combining HOL Induction and Multiway Decision Graphs[J]. Journal of Computer Science and Technology, 2009, 24(1): 76-95.
    [5]Xiao-Ju Dong, Yu-Xi Fu. Barbed Congruence of Asymmetry and Mismatch[J]. Journal of Computer Science and Technology, 2007, 22(4): 575-579.
    [6]LIN Huimin. Computing Bisimulations for Finite-Controlπ-Calculus[J]. Journal of Computer Science and Technology, 2000, 15(1): 1-9.
    [7]WANG Bingshan, LI Zhoujun, CHEN Huowang. Universal Abstract Consistency Class and Universal Refutation[J]. Journal of Computer Science and Technology, 1999, 14(2): 165-172.
    [8]Fu Yuxi. Symmetric π-Calculus[J]. Journal of Computer Science and Technology, 1998, 13(3): 202-208.
    [9]Zheng Yuhua, Xie Li, Sun Zliongxiu. Full Or-Parallemism and Restricted And-Parallelism in BTM[J]. Journal of Computer Science and Technology, 1994, 9(4): 373-381.
    [10]Xue Xing, Sun Zhongxiu, Zhou Jianqiang, Xu Xihao. A Message-Based Distributed Kernel for a Full Heterogeneous Environment[J]. Journal of Computer Science and Technology, 1990, 5(1): 47-56.
    • Supplements (0)

Catalog

    Get Citation
    XML
    Article views (30) PDF downloads (1541) Cited by()
    Related

    Copyright ©2025 JCST, All Rights Reserved     京ICP备05002829号-1

    Institute of Computing Technology, Chinese Academy of Sciences
    P.O. Box 2704, Beijing 100190, P.R. China

    Tel.: 86-10-62610746 E-mail: jcst@ict.ac.cn

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return